\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type, ${\it init}$:$x$:Id fp$\rightarrow$ ${\it ds}$($x$)?Void,\+
\\[0ex]${\it pre}$:$a$:Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;locl($a$))$\rightarrow$Prop,
\\[0ex]${\it ef}$:${\it kx}$:Knd$\times$Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kx}$))$\rightarrow$${\it ds}$(2of(${\it kx}$))?Void,
\\[0ex]${\it send}$:\=${\it kl}$:Knd$\times$IdLnk fp$\rightarrow$\+
\\[0ex](${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kl}$))$\rightarrow$(${\it da}$(rcv(2of(${\it kl}$),${\it tg}$))?Void List))) List,
\-\\[0ex]${\it frame}$:$x$:Id fp$\rightarrow$ Knd List, ${\it sframe}$:${\it ltg}$:IdLnk$\times$Id fp$\rightarrow$ Knd List, ${\it aframe}$:$k$:Knd fp$\rightarrow$ Id List,
\\[0ex]${\it bframe}$:$k$:Knd fp$\rightarrow$ IdLnk List, ${\it rframe}$:$x$:Id fp$\rightarrow$ Knd List.
\-\\[0ex]mk{-}ma(${\it ds}$;
\\[0ex]${\it da}$;
\\[0ex]${\it init}$;
\\[0ex]${\it pre}$;
\\[0ex]${\it ef}$;
\\[0ex]${\it send}$;
\\[0ex]${\it frame}$;
\\[0ex]${\it sframe}$;
\\[0ex]${\it aframe}$;
\\[0ex]${\it bframe}$;
\\[0ex]${\it rframe}$)
\\[0ex]$\in$ MsgA
\end{tabbing}